Nuprl Lemma : SESAxioms_wf 0,22

E:Type{i}, T:(IdIdType{i}), pred?:(E(E+Unit)), info:(E(IdId+(IdLnkE)Id)), when,
after:(x:Ide:ET(loc(e),x)).
SESAxioms{i:l}(ETpred?infowhenafter Prop{i'} 
latex


DefinitionsId, pred(e), loc(e), SESAxioms{i:l}(ETpred?infowhenafter), x:AB(x), P  Q, destination(l), A & B, Prop, SWellFounded(R(x;y)), x,yt(x;y), pred!(e;e'), source(l), rcv?(e), link(e), sender(e), e < e', A, b, first(e), P & Q, IdLnk, Unit, P  Q, x:AB(x), t  T
Lemmasloc wf, pred wf, Id wf, unit wf, IdLnk wf, first wf, assert wf, not wf, cless wf, sender wf, link wf, rcv? wf, lsrc wf, pred! wf, strongwellfounded wf, ldst wf

origin